$\forall$$T$:Type, $l_{1}$,$l_{2}$:($T$ List), $x$:$T$. \\[0ex]iseg($T$; $l_{1}$; append($l_{2}$; cons($x$; []))) \\[0ex]$\Leftarrow\!\Rightarrow$ (iseg($T$; $l_{1}$; $l_{2}$) $\vee$ ($l_{1}$ = append($l_{2}$; cons($x$; []))))